﻿#include "init.h"
//进行SAT_DPLL运算

int SAT_DPLL(PLists& L, int* a, int n, int now)	//SAT主程序
{
	int next = 0;	//方便递归回溯
	if (IsSAT(L))	//全删除，满足
		return OK;
	else
	{
		if (IsUnSAT(L) == OK)	//存在空子句
		{
			removeagain(L, now);	//通过flag=now恢复子句
			if (now > 0)
				a[now] = 0;		//恢复结束后把flag=now的结果设为未解
			else
				a[-now] = 0;
			return FALSE;
		}
		else
		{
			next = OwnSingle(L, n);	//获得单子句文字赋予next
			if (next == 0)
				next = getstandnumb(L, n);	//没有单子句，使用策略获得新关键字
			if (next > 0)
				a[next] = 1;
			if (next < 0)
				a[-next] = -1;
			if (next == 0)
				return FALSE;
			TransToS1(L, next);	//转换成s1
			TransToS2(L, next); //转换成s2

			if (SAT_DPLL(L, a, n, next) == OK)//递归算法	1
				return OK;
			else		//使用关键字简化后得到空子句
			{
				removeagain(L, next);	//通过flag=now恢复子句
				TransToS1(L, -next);	//使用负文字化简
				TransToS2(L, -next);
				if (SAT_DPLL(L, a, n, -next) == OK)				//  2
				{
					if (next > 0)
						a[next] = -1;
					else
						a[-next] = 1;
					return OK;
				}
				else		//此时即某一文字正负均无法进行，即回溯上次过程
				{
					removeagain(L, -next);
					if (next > 0)
						a[next] = 0;
					else
						a[-next] = 0;
					return FALSE;
				}
			}
		}
	}
}

void removeagain(PLists& L, int he)	//根据flag=he恢复结构
{
	PLists sl = L;
	PLists s = sl->next;
	PLists temp = NULL;
	while (s)
	{
		if (s->flag == he)
		{
			s->is = 0;
			s->flag = 0;
			sl = s;
			s = s->next;
			continue;
		}
		PLnode ss = s->elem;
		if (ss)
			ss = ss->next;
		while (ss)
		{
			if (ss->is == 1)
			{
				if (ss->data == -he)
				{
					ss->is = 0;
					s->number++;
				}
				else
					ss->is = 1;
			}
			ss = ss->next;
		}
		sl = s;
		s = sl->next;
	}
}

void TransToS1(PLists& L, int a)	//转换成s1
{
	int stan = 0;
	int op = 0;
	PLists sL = L;
	PLists s = sL->next;
	PLists temp = NULL;
	while (s != NULL)
	{
		if (s->is == 1)
		{
			s = s->next;
			continue;
		}
		PLnode ss = s->elem;
		if (ss)
		{
			ss = ss->next;
		}
		while (ss != NULL)
		{
			if (a == ss->data)
			{
				s->is = 1;
				if (s->flag == 0)
					s->flag = a;
				break;
			}
			ss = ss->next;
		}
		if (s)
		{
			sL = s;
			s = s->next;
		}
	}
}

void TransToS2(PLists& L, int a)	//转换成s2
{
	int re = 0;
	PLists s = L->next;
	while (s != NULL)
	{
		if (s->is == 1)
		{
			s = s->next;
			continue;
		}
		PLnode ss = s->elem;
		if (ss)
		{
			ss = ss->next;
		}
		while (ss != NULL)
		{
			if (-a == ss->data)
			{
				ss->is = 1;
				s->number -= 1;
			}
			ss = ss->next;
		}
		s = s->next;
	}
}

int OwnSingle(PLists& L, int nn)	//获得单子句的文字
{
	PLists s = L->next;
	while (s != NULL)
	{
		if (s->is != 1 && s->number == 1)
		{
			PLnode ss = s->elem->next;
			while (ss)
			{
				if (ss->is == 0)
					return ss->data;
				ss = ss->next;
			}
		}
		s = s->next;
	}
	return FALSE;//返回只有一个的数字
}

int getstandnumb(PLists& L, int n)	//根据出现次数最多获得关键字
{
	int flag = 0;
	int i = 0;
	int* a = (int*)malloc((2 * n + 2) * sizeof(int));
	for (i = 0; i < 2 * n + 1; i++) {
		a[i] = 0;
	}
	PLists s = L->next;
	while (s)
	{
		if (s->is != 1)
		{
			PLnode ss = s->elem;
			if (ss)
			{
				ss = ss->next;
				while (ss)
				{
					if (ss->is != 1 && ss->data > 0)
						a[2 * (ss->data) - 1]++;
					else if (ss->is != 1 && ss->data < 0)
						a[2 * (-(ss->data))]++;
					ss = ss->next;
				}
			}
		}
		s = s->next;
	}
	for (i = 1; i < 2 * n + 1; i++)	//找出出现次数的最大值
	{
		if (a[i] > flag)
			flag = a[i];
	}
	for (i = 1; i < 2 * n + 1; i++)		 //找到变元 
	{
		if (a[i] == flag)
			break;
	}
	free(a);	//释放空间
	if (i % 2)
	{
		return ((i + 1) / 2);
	}
	else
	{
		return (-(i / 2));
	}
}

int IsSAT(PLists& L)	//判断是否满足
{
	PLists s = L->next;
	while (s)
	{
		if (s->is == 0)
			return 0;
		s = s->next;
	}
	return 1;
}

int IsUnSAT(PLists& L)//判断存在空子句
{
	PLists s = L->next;
	while (s)
	{
		if (s->is != 1)
		{
			int i = 0;
			PLnode ss = s->elem;
			if (ss)
				ss = ss->next;
			while (ss)
			{
				if (ss->is == 0)
					i = 1;
				ss = ss->next;
			}
			if (i == 0)
				return 1;
		}
		s = s->next;
	}
	return 0;
}